| | step type | requirements | statement |
| 0 | generalization | 1 | ⊢  |
| 1 | instantiation | 4, 2, 3 | ⊢  |
| | : , : , :  |
| 2 | instantiation | 4, 5, 6 | ⊢  |
| | : , : , :  |
| 3 | instantiation | 7, 8, 9 | ⊢  |
| | : , : , :  |
| 4 | conjecture | | ⊢  |
| | proveit.physics.quantum.circuits.rhs_prob_via_equiv |
| 5 | instantiation | 10, 494, 689, 11, 12, 338, 13, 14, 15, 680, 656, 16, 17* | ⊢  |
| | : , : , : , : , :  |
| 6 | modus ponens | 18, 19 | ⊢  |
| 7 | conjecture | | ⊢  |
| | proveit.physics.quantum.circuits.equiv_transitivity |
| 8 | modus ponens | 20, 21 | ⊢  |
| 9 | instantiation | 34, 22 | ⊢  |
| | : , :  |
| 10 | conjecture | | ⊢  |
| | proveit.physics.quantum.circuits.phase_kickbacks_on_register |
| 11 | instantiation | 584, 23, 467 | ⊢  |
| | : , : , :  |
| 12 | modus ponens | 24, 25 | ⊢  |
| 13 | axiom | | ⊢  |
| | proveit.physics.quantum.QPE._normalized_ket_u |
| 14 | instantiation | 584, 26, 467 | ⊢  |
| | : , : , :  |
| 15 | modus ponens | 27, 28 | ⊢  |
| 16 | instantiation | 263, 679, 264, 75, 76, 77* | ⊢  |
| | : , : , : , : , : , :  |
| 17 | instantiation | 29, 614, 664, 682, 30, 31, 615, 602, 594, 595, 32, 597 | , ⊢  |
| | : , : , : , : , : , :  |
| 18 | instantiation | 51, 610, 527, 33 | ⊢  |
| | : , : , : , : , : , : , : , :  |
| 19 | instantiation | 34, 35 | ⊢  |
| | : , :  |
| 20 | instantiation | 51, 664, 610, 682, 52, 615 | ⊢  |
| | : , : , : , : , : , : , : , :  |
| 21 | instantiation | 578, 36, 37 | ⊢  |
| | : , : , :  |
| 22 | modus ponens | 38, 39 | ⊢  |
| 23 | instantiation | 578, 40, 528 | ⊢  |
| | : , : , :  |
| 24 | instantiation | 471, 676, 677, 472 | ⊢  |
| | : , : , : , :  |
| 25 | generalization | 41 | ⊢  |
| 26 | instantiation | 578, 42, 528 | ⊢  |
| | : , : , :  |
| 27 | instantiation | 471, 676, 677, 472 | ⊢  |
| | : , : , : , :  |
| 28 | generalization | 43 | ⊢  |
| 29 | conjecture | | ⊢  |
| | proveit.numbers.multiplication.disassociation |
| 30 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 31 | instantiation | 631 | ⊢  |
| | : , :  |
| 32 | instantiation | 685, 635, 44 | , ⊢  |
| | : , : , :  |
| 33 | instantiation | 584, 45, 467 | ⊢  |
| | : , : , :  |
| 34 | conjecture | | ⊢  |
| | proveit.physics.quantum.circuits.equiv_reflexivity |
| 35 | instantiation | 46, 494, 689, 64 | ⊢  |
| | : , : , :  |
| 36 | instantiation | 578, 47, 48 | ⊢  |
| | : , : , :  |
| 37 | instantiation | 238, 527, 72, 49, 50 | ⊢  |
| | : , : , : , :  |
| 38 | instantiation | 51, 664, 610, 682, 52, 615 | ⊢  |
| | : , : , : , : , : , : , : , :  |
| 39 | instantiation | 89, 666, 53, 689, 494, 54, 55, 338, 56, 57, 58, 59, 60, 579, 417, 682, 527, 103, 61, 605* | ⊢  |
| | : , : , : , : , : , :  |
| 40 | instantiation | 508, 509 | ⊢  |
| | : , : , :  |
| 41 | instantiation | 62, 63, 435, 64 | , ⊢  |
| | : , : , :  |
| 42 | instantiation | 508, 509 | ⊢  |
| | : , : , :  |
| 43 | instantiation | 65, 123, 627, 66 | , ⊢  |
| | : , : , : , :  |
| 44 | instantiation | 685, 652, 67 | , ⊢  |
| | : , : , :  |
| 45 | instantiation | 578, 68, 528 | ⊢  |
| | : , : , :  |
| 46 | axiom | | ⊢  |
| | proveit.physics.quantum.QPE.QPE1_def |
| 47 | instantiation | 578, 69, 70 | ⊢  |
| | : , : , :  |
| 48 | instantiation | 238, 527, 71, 72, 73 | ⊢  |
| | : , : , : , :  |
| 49 | instantiation | 74, 527 | ⊢  |
| | : , :  |
| 50 | instantiation | 263, 679, 264, 75, 76, 77* | ⊢  |
| | : , : , : , : , : , :  |
| 51 | conjecture | | ⊢  |
| | proveit.physics.quantum.circuits.circuit_equiv_temporal_sub |
| 52 | instantiation | 631 | ⊢  |
| | : , :  |
| 53 | instantiation | 631 | ⊢  |
| | : , :  |
| 54 | instantiation | 631 | ⊢  |
| | : , :  |
| 55 | instantiation | 78, 689 | ⊢  |
| | :  |
| 56 | instantiation | 584, 79, 80 | ⊢  |
| | : , : , :  |
| 57 | instantiation | 492, 81 | ⊢  |
| | : , :  |
| 58 | instantiation | 631 | ⊢  |
| | : , :  |
| 59 | instantiation | 492, 82 | ⊢  |
| | : , :  |
| 60 | instantiation | 584, 83, 84 | ⊢  |
| | : , : , :  |
| 61 | instantiation | 186, 614, 85, 189, 86, 192 | ⊢  |
| | : , :  |
| 62 | conjecture | | ⊢  |
| | proveit.linear_algebra.matrices.exponentiation.U_closure |
| 63 | instantiation | 663, 664, 87 | , ⊢  |
| | : , :  |
| 64 | axiom | | ⊢  |
| | proveit.physics.quantum.QPE._unitary_U |
| 65 | conjecture | | ⊢  |
| | proveit.linear_algebra.matrices.exponentiation.unital2pi_eigen_exp_application |
| 66 | axiom | | ⊢  |
| | proveit.physics.quantum.QPE._eigen_uu |
| 67 | instantiation | 685, 655, 88 | , ⊢  |
| | : , : , :  |
| 68 | instantiation | 508, 509 | ⊢  |
| | : , : , :  |
| 69 | instantiation | 89, 364, 90, 687, 91, 494, 92, 93, 94, 338, 95, 96, 97, 98, 99, 100, 101, 579, 176, 682, 102, 103, 104, 605, 327*, 105*, 106* | ⊢  |
| | : , : , : , : , : , :  |
| 70 | instantiation | 238, 527, 107, 108, 109, 110* | ⊢  |
| | : , : , : , :  |
| 71 | instantiation | 584, 111, 467 | ⊢  |
| | : , : , :  |
| 72 | instantiation | 584, 112, 467 | ⊢  |
| | : , : , :  |
| 73 | instantiation | 282, 283, 284, 371* | ⊢  |
| | : , : , : , :  |
| 74 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.range_from1_len_typical_eq |
| 75 | instantiation | 492, 113 | ⊢  |
| | : , :  |
| 76 | instantiation | 492, 114 | ⊢  |
| | : , :  |
| 77 | instantiation | 584, 115, 116 | , ⊢  |
| | : , : , :  |
| 78 | conjecture | | ⊢  |
| | proveit.physics.quantum.QPE._psi_t_ket_register |
| 79 | instantiation | 117 | ⊢  |
| | : , : , :  |
| 80 | instantiation | 492, 118 | ⊢  |
| | : , :  |
| 81 | instantiation | 218, 119, 605 | ⊢  |
| | : , : , :  |
| 82 | instantiation | 270, 119, 417 | ⊢  |
| | : , : , :  |
| 83 | instantiation | 120 | ⊢  |
| | : , :  |
| 84 | instantiation | 492, 121 | ⊢  |
| | : , :  |
| 85 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 86 | instantiation | 492, 481 | ⊢  |
| | : , :  |
| 87 | instantiation | 667, 122 | , ⊢  |
| | :  |
| 88 | instantiation | 685, 686, 123 | , ⊢  |
| | : , : , :  |
| 89 | conjecture | | ⊢  |
| | proveit.physics.quantum.circuits.output_consolidation |
| 90 | instantiation | 584, 124, 134 | ⊢  |
| | : , : , :  |
| 91 | instantiation | 468, 654, 677, 687, 279 | ⊢  |
| | : , : , :  |
| 92 | instantiation | 584, 125, 134 | ⊢  |
| | : , : , :  |
| 93 | instantiation | 526, 126, 209 | ⊢  |
| | : , : , :  |
| 94 | modus ponens | 127, 128 | ⊢  |
| 95 | instantiation | 584, 129, 130 | ⊢  |
| | : , : , :  |
| 96 | instantiation | 492, 131 | ⊢  |
| | : , :  |
| 97 | instantiation | 492, 132 | ⊢  |
| | : , :  |
| 98 | instantiation | 584, 133, 134 | ⊢  |
| | : , : , :  |
| 99 | instantiation | 492, 135 | ⊢  |
| | : , :  |
| 100 | instantiation | 492, 136 | ⊢  |
| | : , :  |
| 101 | instantiation | 584, 137, 138 | ⊢  |
| | : , : , :  |
| 102 | modus ponens | 139, 140 | ⊢  |
| 103 | instantiation | 685, 543, 141 | ⊢  |
| | : , : , :  |
| 104 | instantiation | 142, 664, 358, 610, 143, 426, 144, 145 | ⊢  |
| | : , : , : , : , : , :  |
| 105 | instantiation | 584, 146, 147 | ⊢  |
| | : , : , :  |
| 106 | instantiation | 584, 148, 198 | ⊢  |
| | : , : , :  |
| 107 | instantiation | 584, 149, 467 | ⊢  |
| | : , : , :  |
| 108 | instantiation | 584, 150, 467 | ⊢  |
| | : , : , :  |
| 109 | instantiation | 282, 283, 284, 151* | ⊢  |
| | : , : , : , :  |
| 110 | instantiation | 245, 152 | , ⊢  |
| | : , :  |
| 111 | instantiation | 328, 666, 153, 330, 344, 331, 358, 332* | ⊢  |
| | : , : , : , :  |
| 112 | instantiation | 578, 154, 528 | ⊢  |
| | : , : , :  |
| 113 | instantiation | 584, 155, 371 | ⊢  |
| | : , : , :  |
| 114 | instantiation | 584, 156, 481 | ⊢  |
| | : , : , :  |
| 115 | instantiation | 609, 682, 664, 610, 615, 157, 158, 582, 617 | , ⊢  |
| | : , : , : , : , : , :  |
| 116 | instantiation | 587, 617, 158 | , ⊢  |
| | : , :  |
| 117 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_3 |
| 118 | instantiation | 578, 159, 248 | ⊢  |
| | : , : , :  |
| 119 | instantiation | 526, 664, 160 | ⊢  |
| | : , : , :  |
| 120 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_2 |
| 121 | instantiation | 578, 161, 249 | ⊢  |
| | : , : , :  |
| 122 | instantiation | 669, 453, 162 | , ⊢  |
| | :  |
| 123 | instantiation | 663, 664, 163 | , ⊢  |
| | : , :  |
| 124 | instantiation | 328, 210, 164, 180, 213, 331, 358, 181* | ⊢  |
| | : , : , : , :  |
| 125 | instantiation | 328, 210, 165, 180, 213, 331, 358, 181* | ⊢  |
| | : , : , : , :  |
| 126 | instantiation | 532, 533, 496, 166 | ⊢  |
| | : , : , : , :  |
| 127 | instantiation | 471, 654, 677, 279 | ⊢  |
| | : , : , : , :  |
| 128 | generalization | 167 | ⊢  |
| 129 | instantiation | 584, 168, 169 | ⊢  |
| | : , : , :  |
| 130 | instantiation | 492, 170 | ⊢  |
| | : , :  |
| 131 | instantiation | 218, 175, 605 | ⊢  |
| | : , : , :  |
| 132 | instantiation | 238, 527, 222, 171, 172 | ⊢  |
| | : , : , : , :  |
| 133 | instantiation | 328, 210, 173, 180, 213, 331, 358, 181* | ⊢  |
| | : , : , : , :  |
| 134 | instantiation | 492, 174 | ⊢  |
| | : , :  |
| 135 | instantiation | 270, 175, 176 | ⊢  |
| | : , : , :  |
| 136 | instantiation | 584, 177, 178 | ⊢  |
| | : , : , :  |
| 137 | instantiation | 328, 210, 179, 180, 213, 331, 358, 181* | ⊢  |
| | : , : , : , :  |
| 138 | instantiation | 492, 182 | ⊢  |
| | : , :  |
| 139 | instantiation | 471, 676, 677, 472 | ⊢  |
| | : , : , : , :  |
| 140 | generalization | 183 | ⊢  |
| 141 | instantiation | 406, 689, 494 | ⊢  |
| | : , :  |
| 142 | conjecture | | ⊢  |
| | proveit.logic.booleans.conjunction.disassociate |
| 143 | instantiation | 631 | ⊢  |
| | : , :  |
| 144 | instantiation | 584, 184, 185 | ⊢  |
| | : , : , :  |
| 145 | instantiation | 186, 187, 188, 189, 190, 191, 192 | ⊢  |
| | : , :  |
| 146 | instantiation | 576, 193 | ⊢  |
| | : , : , :  |
| 147 | instantiation | 492, 194 | ⊢  |
| | : , :  |
| 148 | instantiation | 576, 605 | ⊢  |
| | : , : , :  |
| 149 | instantiation | 328, 666, 195, 330, 344, 331, 358, 332* | ⊢  |
| | : , : , : , :  |
| 150 | instantiation | 578, 196, 528 | ⊢  |
| | : , : , :  |
| 151 | instantiation | 584, 197, 198 | ⊢  |
| | : , : , :  |
| 152 | instantiation | 199, 200, 201 | , ⊢  |
| | :  |
| 153 | instantiation | 631 | ⊢  |
| | : , :  |
| 154 | instantiation | 508, 509 | ⊢  |
| | : , : , :  |
| 155 | instantiation | 576, 583 | ⊢  |
| | : , : , :  |
| 156 | instantiation | 576, 583 | ⊢  |
| | : , : , :  |
| 157 | instantiation | 631 | ⊢  |
| | : , :  |
| 158 | instantiation | 685, 635, 202 | , ⊢  |
| | : , : , :  |
| 159 | instantiation | 508, 203 | ⊢  |
| | : , : , :  |
| 160 | instantiation | 584, 204, 439 | ⊢  |
| | : , : , :  |
| 161 | instantiation | 508, 205 | ⊢  |
| | : , : , :  |
| 162 | instantiation | 673, 676, 677, 483 | , ⊢  |
| | : , : , :  |
| 163 | instantiation | 667, 206 | , ⊢  |
| | :  |
| 164 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 165 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 166 | instantiation | 514, 533, 515, 207 | ⊢  |
| | : , : , : , :  |
| 167 | instantiation | 526, 208, 209 | , ⊢  |
| | : , : , :  |
| 168 | instantiation | 328, 210, 211, 212, 213, 331, 509, 214* | ⊢  |
| | : , : , : , :  |
| 169 | instantiation | 492, 215 | ⊢  |
| | : , :  |
| 170 | instantiation | 578, 216, 304 | ⊢  |
| | : , : , :  |
| 171 | instantiation | 584, 217, 467 | ⊢  |
| | : , : , :  |
| 172 | instantiation | 218, 283, 353, 371* | ⊢  |
| | : , : , :  |
| 173 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 174 | instantiation | 510, 321 | ⊢  |
| | : , :  |
| 175 | instantiation | 526, 321, 219 | ⊢  |
| | : , : , :  |
| 176 | instantiation | 584, 220, 221 | ⊢  |
| | : , : , :  |
| 177 | instantiation | 238, 527, 222, 224, 223 | ⊢  |
| | : , : , : , :  |
| 178 | instantiation | 238, 527, 224, 225, 226 | ⊢  |
| | : , : , : , :  |
| 179 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 180 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 181 | instantiation | 584, 227, 228 | ⊢  |
| | : , : , :  |
| 182 | instantiation | 578, 229, 322 | ⊢  |
| | : , : , :  |
| 183 | instantiation | 553, 230, 231 | , ⊢  |
| | :  |
| 184 | instantiation | 578, 232, 426 | ⊢  |
| | : , : , :  |
| 185 | instantiation | 492, 233 | ⊢  |
| | : , :  |
| 186 | conjecture | | ⊢  |
| | proveit.logic.booleans.conjunction.and_if_all |
| 187 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.nat4 |
| 188 | instantiation | 234 | ⊢  |
| | : , : , : , :  |
| 189 | instantiation | 237 | ⊢  |
| | :  |
| 190 | instantiation | 492, 605 | ⊢  |
| | : , :  |
| 191 | modus ponens | 235, 236 | ⊢  |
| 192 | instantiation | 237 | ⊢  |
| | :  |
| 193 | instantiation | 238, 527, 239, 385, 240 | ⊢  |
| | : , : , : , :  |
| 194 | instantiation | 576, 241, 242* | ⊢  |
| | : , : , :  |
| 195 | instantiation | 631 | ⊢  |
| | : , :  |
| 196 | instantiation | 508, 509 | ⊢  |
| | : , : , :  |
| 197 | instantiation | 422, 614, 243, 244, 371, 562 | ⊢  |
| | : , : , : , :  |
| 198 | instantiation | 245, 687 | ⊢  |
| | : , :  |
| 199 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.pos_int_is_natural_pos |
| 200 | instantiation | 678, 670, 656 | , ⊢  |
| | : , :  |
| 201 | instantiation | 323, 324, 246 | , ⊢  |
| | : , : , :  |
| 202 | instantiation | 685, 652, 247 | , ⊢  |
| | : , : , :  |
| 203 | instantiation | 526, 614, 248 | ⊢  |
| | : , : , :  |
| 204 | instantiation | 576, 407 | ⊢  |
| | : , : , :  |
| 205 | instantiation | 526, 664, 249 | ⊢  |
| | : , : , :  |
| 206 | instantiation | 669, 250, 251 | , ⊢  |
| | :  |
| 207 | instantiation | 532, 533, 252, 535 | ⊢  |
| | : , : , : , :  |
| 208 | instantiation | 532, 533, 496, 253 | , ⊢  |
| | : , : , : , :  |
| 209 | instantiation | 576, 254 | ⊢  |
| | : , : , :  |
| 210 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat3 |
| 211 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 212 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 213 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 214 | instantiation | 584, 255, 256 | ⊢  |
| | : , : , :  |
| 215 | instantiation | 606, 617, 602 | ⊢  |
| | : , :  |
| 216 | instantiation | 508, 257 | ⊢  |
| | : , : , :  |
| 217 | instantiation | 328, 666, 258, 330, 344, 331, 358, 332* | ⊢  |
| | : , : , : , :  |
| 218 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.partition_front |
| 219 | instantiation | 584, 259, 260 | ⊢  |
| | : , : , :  |
| 220 | instantiation | 609, 682, 664, 610, 615, 477, 617, 619, 618 | ⊢  |
| | : , : , : , : , : , :  |
| 221 | instantiation | 261, 619, 617 | ⊢  |
| | : , :  |
| 222 | instantiation | 584, 262, 467 | ⊢  |
| | : , : , :  |
| 223 | instantiation | 263, 571, 264, 265, 266, 267* | ⊢  |
| | : , : , : , : , : , :  |
| 224 | instantiation | 584, 268, 467 | ⊢  |
| | : , : , :  |
| 225 | instantiation | 584, 269, 467 | ⊢  |
| | : , : , :  |
| 226 | instantiation | 270, 271, 579, 272* | ⊢  |
| | : , : , :  |
| 227 | instantiation | 422, 614, 273, 274, 425, 426 | ⊢  |
| | : , : , : , :  |
| 228 | instantiation | 584, 275, 276 | ⊢  |
| | : , : , :  |
| 229 | instantiation | 508, 277 | ⊢  |
| | : , : , :  |
| 230 | instantiation | 678, 453, 656 | , ⊢  |
| | : , :  |
| 231 | instantiation | 511, 278 | , ⊢  |
| | : , :  |
| 232 | instantiation | 508, 358 | ⊢  |
| | : , : , :  |
| 233 | instantiation | 510, 536 | ⊢  |
| | : , :  |
| 234 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_4_typical_eq |
| 235 | instantiation | 471, 654, 677, 279 | ⊢  |
| | : , : , : , :  |
| 236 | generalization | 280 | ⊢  |
| 237 | axiom | | ⊢  |
| | proveit.logic.equality.equals_reflexivity |
| 238 | conjecture | | ⊢  |
| | proveit.core_expr_types.operations.operands_substitution_via_tuple |
| 239 | instantiation | 584, 281, 467 | ⊢  |
| | : , : , :  |
| 240 | instantiation | 282, 283, 284, 562* | ⊢  |
| | : , : , : , :  |
| 241 | instantiation | 285, 689 | ⊢  |
| | :  |
| 242 | modus ponens | 286, 287 | ⊢  |
| 243 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 244 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 245 | conjecture | | ⊢  |
| | proveit.physics.quantum.circuits.unary_multi_output_reduction |
| 246 | instantiation | 367, 633, 368, 288, 289, 371* | , ⊢  |
| | : , : , :  |
| 247 | instantiation | 685, 655, 290 | , ⊢  |
| | : , : , :  |
| 248 | instantiation | 584, 291, 292 | ⊢  |
| | : , : , :  |
| 249 | instantiation | 584, 293, 294 | ⊢  |
| | : , : , :  |
| 250 | instantiation | 685, 672, 295 | , ⊢  |
| | : , : , :  |
| 251 | instantiation | 673, 676, 677, 295 | , ⊢  |
| | : , : , :  |
| 252 | instantiation | 685, 551, 296 | ⊢  |
| | : , : , :  |
| 253 | instantiation | 514, 533, 515, 297 | , ⊢  |
| | : , : , : , :  |
| 254 | instantiation | 298, 602 | ⊢  |
| | :  |
| 255 | instantiation | 422, 614, 299, 300, 425, 528 | ⊢  |
| | : , : , : , :  |
| 256 | instantiation | 584, 301, 302 | ⊢  |
| | : , : , :  |
| 257 | instantiation | 526, 303, 304 | ⊢  |
| | : , : , :  |
| 258 | instantiation | 631 | ⊢  |
| | : , :  |
| 259 | instantiation | 576, 407 | ⊢  |
| | : , : , :  |
| 260 | instantiation | 584, 305, 306 | ⊢  |
| | : , : , :  |
| 261 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_triple_23 |
| 262 | instantiation | 578, 307, 528 | ⊢  |
| | : , : , :  |
| 263 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.shift_equivalence |
| 264 | instantiation | 526, 527, 308 | ⊢  |
| | : , : , :  |
| 265 | instantiation | 492, 309 | ⊢  |
| | : , :  |
| 266 | instantiation | 492, 310 | ⊢  |
| | : , :  |
| 267 | instantiation | 609, 682, 664, 610, 615, 311, 312, 618, 617 | , ⊢  |
| | : , : , : , : , : , :  |
| 268 | instantiation | 578, 313, 401 | ⊢  |
| | : , : , :  |
| 269 | instantiation | 314, 315, 316* | ⊢  |
| | : , : , : , :  |
| 270 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.partition_back |
| 271 | instantiation | 526, 317, 318 | ⊢  |
| | : , : , :  |
| 272 | instantiation | 319, 619, 617 | ⊢  |
| | : , :  |
| 273 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 274 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 275 | instantiation | 609, 610, 664, 611, 619, 617, 618 | ⊢  |
| | : , : , : , : , : , :  |
| 276 | instantiation | 320, 682, 610, 615, 619, 617 | ⊢  |
| | : , : , : , : , : , : , :  |
| 277 | instantiation | 526, 321, 322 | ⊢  |
| | : , : , :  |
| 278 | instantiation | 323, 324, 325 | , ⊢  |
| | : , : , :  |
| 279 | instantiation | 526, 326, 605 | ⊢  |
| | : , : , :  |
| 280 | instantiation | 492, 327 | , ⊢  |
| | : , :  |
| 281 | instantiation | 328, 666, 329, 330, 344, 331, 358, 332* | ⊢  |
| | : , : , : , :  |
| 282 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.merge_front |
| 283 | instantiation | 526, 536, 333 | ⊢  |
| | : , : , :  |
| 284 | instantiation | 492, 353 | ⊢  |
| | : , :  |
| 285 | axiom | | ⊢  |
| | proveit.physics.quantum.QPE._psi_t_def |
| 286 | instantiation | 334, 682, 509, 610, 335, 615, 528, 385 | ⊢  |
| | : , : , : , : , : , : , : , :  |
| 287 | instantiation | 384, 666, 381, 382, 383, 336, 337, 338 | ⊢  |
| | : , : , : , :  |
| 288 | instantiation | 685, 652, 339 | , ⊢  |
| | : , : , :  |
| 289 | instantiation | 410, 676, 677, 674 | , ⊢  |
| | : , : , :  |
| 290 | instantiation | 685, 340, 341 | , ⊢  |
| | : , : , :  |
| 291 | instantiation | 576, 407 | ⊢  |
| | : , : , :  |
| 292 | instantiation | 540, 682, 664, 610, 615, 342, 602, 612, 619, 343* | ⊢  |
| | : , : , : , : , : , :  |
| 293 | instantiation | 576, 407 | ⊢  |
| | : , : , :  |
| 294 | instantiation | 540, 682, 664, 610, 615, 344, 619, 612, 345* | ⊢  |
| | : , : , : , : , : , :  |
| 295 | assumption | | ⊢  |
| 296 | instantiation | 568, 569, 346 | ⊢  |
| | : , :  |
| 297 | instantiation | 532, 533, 347, 535 | , ⊢  |
| | : , : , : , :  |
| 298 | conjecture | | ⊢  |
| | proveit.numbers.exponentiation.complex_x_to_first_power_is_x |
| 299 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 300 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 301 | instantiation | 558, 610, 682, 615, 619, 617 | ⊢  |
| | : , : , : , : , : , : , :  |
| 302 | instantiation | 540, 682, 664, 610, 615, 445, 619, 617, 603* | ⊢  |
| | : , : , : , : , : , :  |
| 303 | instantiation | 685, 543, 348 | ⊢  |
| | : , : , :  |
| 304 | instantiation | 584, 349, 350 | ⊢  |
| | : , : , :  |
| 305 | instantiation | 609, 682, 664, 610, 615, 477, 617, 619, 612 | ⊢  |
| | : , : , : , : , : , :  |
| 306 | instantiation | 613, 664, 682, 477, 615, 617, 619 | ⊢  |
| | : , : , : , :  |
| 307 | instantiation | 508, 509 | ⊢  |
| | : , : , :  |
| 308 | instantiation | 584, 351, 378 | ⊢  |
| | : , : , :  |
| 309 | instantiation | 584, 352, 353 | ⊢  |
| | : , : , :  |
| 310 | instantiation | 584, 354, 605 | ⊢  |
| | : , : , :  |
| 311 | instantiation | 631 | ⊢  |
| | : , :  |
| 312 | instantiation | 685, 635, 355 | , ⊢  |
| | : , : , :  |
| 313 | instantiation | 508, 356 | ⊢  |
| | : , : , :  |
| 314 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.extended_range_len |
| 315 | instantiation | 357, 358 | ⊢  |
| | : , : , :  |
| 316 | instantiation | 584, 359, 360 | ⊢  |
| | : , : , :  |
| 317 | instantiation | 578, 536, 361 | ⊢  |
| | : , : , :  |
| 318 | instantiation | 584, 362, 363 | ⊢  |
| | : , : , :  |
| 319 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_triple_12 |
| 320 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_general |
| 321 | instantiation | 685, 543, 364 | ⊢  |
| | : , : , :  |
| 322 | instantiation | 584, 365, 366 | ⊢  |
| | : , : , :  |
| 323 | conjecture | | ⊢  |
| | proveit.numbers.ordering.transitivity_less_less_eq |
| 324 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.less_0_1 |
| 325 | instantiation | 367, 633, 368, 369, 370, 371* | , ⊢  |
| | : , : , :  |
| 326 | instantiation | 372, 607, 634, 630, 373, 374* | ⊢  |
| | : , : , :  |
| 327 | instantiation | 584, 375, 376 | , ⊢  |
| | : , : , :  |
| 328 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.general_len |
| 329 | instantiation | 631 | ⊢  |
| | : , :  |
| 330 | instantiation | 631 | ⊢  |
| | : , :  |
| 331 | instantiation | 526, 610, 425 | ⊢  |
| | : , : , :  |
| 332 | instantiation | 584, 377, 378 | ⊢  |
| | : , : , :  |
| 333 | instantiation | 584, 379, 380 | ⊢  |
| | : , : , :  |
| 334 | conjecture | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_disassociation |
| 335 | instantiation | 431, 666, 381, 382, 383 | ⊢  |
| | : , : , :  |
| 336 | instantiation | 631 | ⊢  |
| | : , :  |
| 337 | instantiation | 384, 432, 528, 433, 434, 385, 386 | ⊢  |
| | : , : , : , :  |
| 338 | axiom | | ⊢  |
| | proveit.physics.quantum.QPE._u_ket_register |
| 339 | instantiation | 685, 655, 670 | , ⊢  |
| | : , : , :  |
| 340 | instantiation | 675, 680, 656 | ⊢  |
| | : , :  |
| 341 | assumption | | ⊢  |
| 342 | instantiation | 631 | ⊢  |
| | : , :  |
| 343 | instantiation | 584, 387, 388 | ⊢  |
| | : , : , :  |
| 344 | instantiation | 631 | ⊢  |
| | : , :  |
| 345 | instantiation | 584, 389, 603 | ⊢  |
| | : , : , :  |
| 346 | instantiation | 591, 592, 390, 602, 594, 595, 391, 597 | ⊢  |
| | : , :  |
| 347 | instantiation | 685, 551, 392 | , ⊢  |
| | : , : , :  |
| 348 | instantiation | 406, 689, 666 | ⊢  |
| | : , :  |
| 349 | instantiation | 576, 407 | ⊢  |
| | : , : , :  |
| 350 | instantiation | 584, 393, 394 | ⊢  |
| | : , : , :  |
| 351 | instantiation | 584, 395, 396 | ⊢  |
| | : , : , :  |
| 352 | instantiation | 576, 399 | ⊢  |
| | : , : , :  |
| 353 | instantiation | 584, 397, 398 | ⊢  |
| | : , : , :  |
| 354 | instantiation | 576, 399 | ⊢  |
| | : , : , :  |
| 355 | instantiation | 685, 652, 400 | , ⊢  |
| | : , : , :  |
| 356 | instantiation | 526, 527, 401 | ⊢  |
| | : , : , :  |
| 357 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.range_len_is_nat |
| 358 | instantiation | 526, 536, 426 | ⊢  |
| | : , : , :  |
| 359 | instantiation | 576, 488 | ⊢  |
| | : , : , :  |
| 360 | instantiation | 584, 402, 403 | ⊢  |
| | : , : , :  |
| 361 | instantiation | 606, 617, 618 | ⊢  |
| | : , :  |
| 362 | instantiation | 576, 488 | ⊢  |
| | : , : , :  |
| 363 | instantiation | 584, 404, 405 | ⊢  |
| | : , : , :  |
| 364 | instantiation | 406, 689, 687 | ⊢  |
| | : , :  |
| 365 | instantiation | 576, 407 | ⊢  |
| | : , : , :  |
| 366 | instantiation | 613, 610, 617, 619 | ⊢  |
| | : , : , : , :  |
| 367 | conjecture | | ⊢  |
| | proveit.numbers.addition.weak_bound_via_left_term_bound |
| 368 | instantiation | 685, 652, 408 | ⊢  |
| | : , : , :  |
| 369 | instantiation | 685, 652, 409 | , ⊢  |
| | : , : , :  |
| 370 | instantiation | 410, 676, 677, 483 | , ⊢  |
| | : , : , :  |
| 371 | instantiation | 584, 411, 412 | ⊢  |
| | : , : , :  |
| 372 | conjecture | | ⊢  |
| | proveit.numbers.ordering.less_eq_shift_add_right |
| 373 | instantiation | 413, 634, 649, 633, 573, 414, 415*, 416* | ⊢  |
| | : , : , :  |
| 374 | instantiation | 578, 417, 418 | ⊢  |
| | : , : , :  |
| 375 | instantiation | 609, 682, 614, 610, 615, 419, 421, 618, 617, 619 | , ⊢  |
| | : , : , : , : , : , :  |
| 376 | instantiation | 420, 610, 682, 615, 421, 619, 617 | , ⊢  |
| | : , : , : , : , : , : , :  |
| 377 | instantiation | 422, 664, 423, 424, 425, 426 | ⊢  |
| | : , : , : , :  |
| 378 | instantiation | 584, 427, 428 | ⊢  |
| | : , : , :  |
| 379 | instantiation | 576, 562 | ⊢  |
| | : , : , :  |
| 380 | instantiation | 584, 429, 430 | ⊢  |
| | : , : , :  |
| 381 | instantiation | 631 | ⊢  |
| | : , :  |
| 382 | instantiation | 431, 432, 528, 433, 434 | ⊢  |
| | : , : , :  |
| 383 | instantiation | 550, 435 | ⊢  |
| | :  |
| 384 | conjecture | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space |
| 385 | instantiation | 584, 436, 467 | ⊢  |
| | : , : , :  |
| 386 | modus ponens | 437, 438 | ⊢  |
| 387 | instantiation | 576, 439 | ⊢  |
| | : , : , :  |
| 388 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.add_2_1 |
| 389 | instantiation | 576, 440 | ⊢  |
| | : , : , :  |
| 390 | instantiation | 624 | ⊢  |
| | : , : , : , : , :  |
| 391 | instantiation | 685, 635, 441 | ⊢  |
| | : , : , :  |
| 392 | instantiation | 568, 569, 442 | , ⊢  |
| | : , :  |
| 393 | instantiation | 584, 443, 444 | ⊢  |
| | : , : , :  |
| 394 | instantiation | 540, 610, 664, 682, 445, 615, 617, 619, 603* | ⊢  |
| | : , : , : , : , : , :  |
| 395 | instantiation | 576, 605 | ⊢  |
| | : , : , :  |
| 396 | instantiation | 576, 562 | ⊢  |
| | : , : , :  |
| 397 | instantiation | 609, 682, 664, 610, 615, 454, 582, 619 | ⊢  |
| | : , : , : , : , : , :  |
| 398 | instantiation | 540, 610, 664, 682, 445, 615, 582, 619, 603* | ⊢  |
| | : , : , : , : , : , :  |
| 399 | instantiation | 608, 619 | ⊢  |
| | :  |
| 400 | instantiation | 685, 655, 446 | , ⊢  |
| | : , : , :  |
| 401 | instantiation | 584, 447, 448 | ⊢  |
| | : , : , :  |
| 402 | instantiation | 584, 449, 450 | ⊢  |
| | : , : , :  |
| 403 | instantiation | 587, 602, 617 | ⊢  |
| | : , :  |
| 404 | instantiation | 584, 451, 452 | ⊢  |
| | : , : , :  |
| 405 | instantiation | 540, 682, 664, 610, 615, 541, 619, 559, 617, 577* | ⊢  |
| | : , : , : , : , : , :  |
| 406 | conjecture | | ⊢  |
| | proveit.numbers.addition.add_nat_pos_closure_bin |
| 407 | conjecture | | ⊢  |
| | proveit.numbers.negation.negated_zero |
| 408 | instantiation | 685, 655, 676 | ⊢  |
| | : , : , :  |
| 409 | instantiation | 685, 655, 453 | , ⊢  |
| | : , : , :  |
| 410 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.interval_lower_bound |
| 411 | instantiation | 609, 682, 664, 610, 615, 454, 582, 619, 617 | ⊢  |
| | : , : , : , : , : , :  |
| 412 | instantiation | 455, 617, 619 | ⊢  |
| | : , :  |
| 413 | conjecture | | ⊢  |
| | proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound |
| 414 | instantiation | 511, 456 | ⊢  |
| | : , :  |
| 415 | instantiation | 458, 619, 617, 457* | ⊢  |
| | : , :  |
| 416 | instantiation | 458, 619, 459* | ⊢  |
| | : , :  |
| 417 | instantiation | 604, 619, 602, 603 | ⊢  |
| | : , : , :  |
| 418 | instantiation | 606, 602, 618 | ⊢  |
| | : , :  |
| 419 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 420 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_general_rev |
| 421 | instantiation | 685, 635, 460 | , ⊢  |
| | : , : , :  |
| 422 | axiom | | ⊢  |
| | proveit.core_expr_types.operations.operands_substitution |
| 423 | instantiation | 631 | ⊢  |
| | : , :  |
| 424 | instantiation | 631 | ⊢  |
| | : , :  |
| 425 | instantiation | 540, 682, 664, 610, 615, 461, 619, 618, 462* | ⊢  |
| | : , : , : , : , : , :  |
| 426 | instantiation | 584, 463, 464 | ⊢  |
| | : , : , :  |
| 427 | instantiation | 609, 610, 664, 682, 611, 615, 619, 617, 618 | ⊢  |
| | : , : , : , : , : , :  |
| 428 | instantiation | 465, 619, 617 | ⊢  |
| | : , :  |
| 429 | instantiation | 609, 610, 664, 682, 611, 615, 612, 617, 618 | ⊢  |
| | : , : , : , : , : , :  |
| 430 | instantiation | 613, 682, 664, 615, 611, 617, 618 | ⊢  |
| | : , : , : , :  |
| 431 | conjecture | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space |
| 432 | instantiation | 526, 689, 528 | ⊢  |
| | : , : , :  |
| 433 | instantiation | 584, 466, 467 | ⊢  |
| | : , : , :  |
| 434 | instantiation | 468, 676, 677, 533, 472 | ⊢  |
| | : , : , :  |
| 435 | instantiation | 663, 664, 469 | ⊢  |
| | : , :  |
| 436 | instantiation | 578, 470, 528 | ⊢  |
| | : , : , :  |
| 437 | instantiation | 471, 676, 677, 472 | ⊢  |
| | : , : , : , :  |
| 438 | generalization | 473 | ⊢  |
| 439 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.add_2_0 |
| 440 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.add_1_0 |
| 441 | instantiation | 685, 652, 474 | ⊢  |
| | : , : , :  |
| 442 | instantiation | 591, 592, 593, 602, 594, 595, 475, 597 | , ⊢  |
| | : , :  |
| 443 | instantiation | 609, 682, 664, 615, 477, 476, 617, 619, 612 | ⊢  |
| | : , : , : , : , : , :  |
| 444 | instantiation | 613, 664, 610, 477, 617, 619 | ⊢  |
| | : , : , : , :  |
| 445 | instantiation | 631 | ⊢  |
| | : , :  |
| 446 | instantiation | 685, 478, 479 | , ⊢  |
| | : , : , :  |
| 447 | instantiation | 576, 488 | ⊢  |
| | : , : , :  |
| 448 | instantiation | 584, 480, 481 | ⊢  |
| | : , : , :  |
| 449 | instantiation | 609, 610, 664, 557, 612, 617, 559, 602 | ⊢  |
| | : , : , : , : , : , :  |
| 450 | instantiation | 613, 682, 614, 615, 482, 617, 559, 602 | ⊢  |
| | : , : , : , :  |
| 451 | instantiation | 609, 610, 664, 682, 557, 615, 619, 617, 559 | ⊢  |
| | : , : , : , : , : , :  |
| 452 | instantiation | 558, 610, 682, 615, 619, 617, 559 | ⊢  |
| | : , : , : , : , : , : , :  |
| 453 | instantiation | 685, 672, 483 | , ⊢  |
| | : , : , :  |
| 454 | instantiation | 631 | ⊢  |
| | : , :  |
| 455 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_triple_31 |
| 456 | instantiation | 546, 598 | ⊢  |
| | :  |
| 457 | instantiation | 484, 617 | ⊢  |
| | :  |
| 458 | conjecture | | ⊢  |
| | proveit.numbers.multiplication.mult_neg_left |
| 459 | instantiation | 485, 619 | ⊢  |
| | :  |
| 460 | instantiation | 685, 652, 486 | , ⊢  |
| | : , : , :  |
| 461 | instantiation | 631 | ⊢  |
| | : , :  |
| 462 | instantiation | 584, 487, 605 | ⊢  |
| | : , : , :  |
| 463 | instantiation | 576, 488 | ⊢  |
| | : , : , :  |
| 464 | instantiation | 584, 489, 490 | ⊢  |
| | : , : , :  |
| 465 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_triple_13 |
| 466 | instantiation | 578, 491, 528 | ⊢  |
| | : , : , :  |
| 467 | instantiation | 492, 493 | ⊢  |
| | : , :  |
| 468 | conjecture | | ⊢  |
| | proveit.logic.booleans.conjunction.redundant_conjunction_general |
| 469 | instantiation | 685, 543, 494 | ⊢  |
| | : , : , :  |
| 470 | instantiation | 508, 509 | ⊢  |
| | : , : , :  |
| 471 | conjecture | | ⊢  |
| | proveit.logic.booleans.conjunction.conjunction_from_quantification |
| 472 | instantiation | 526, 495, 605 | ⊢  |
| | : , : , :  |
| 473 | instantiation | 532, 533, 496, 497 | , ⊢  |
| | : , : , : , :  |
| 474 | instantiation | 685, 655, 498 | ⊢  |
| | : , : , :  |
| 475 | instantiation | 685, 635, 499 | , ⊢  |
| | : , : , :  |
| 476 | instantiation | 631 | ⊢  |
| | : , :  |
| 477 | instantiation | 631 | ⊢  |
| | : , :  |
| 478 | instantiation | 675, 654, 680 | ⊢  |
| | : , :  |
| 479 | assumption | | ⊢  |
| 480 | instantiation | 584, 500, 501 | ⊢  |
| | : , : , :  |
| 481 | instantiation | 502, 617 | ⊢  |
| | :  |
| 482 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 483 | assumption | | ⊢  |
| 484 | conjecture | | ⊢  |
| | proveit.numbers.multiplication.elim_one_left |
| 485 | conjecture | | ⊢  |
| | proveit.numbers.multiplication.elim_one_right |
| 486 | instantiation | 685, 655, 503 | , ⊢  |
| | : , : , :  |
| 487 | instantiation | 576, 579 | ⊢  |
| | : , : , :  |
| 488 | instantiation | 581, 582, 602, 583* | ⊢  |
| | : , :  |
| 489 | instantiation | 584, 504, 505 | ⊢  |
| | : , : , :  |
| 490 | instantiation | 540, 610, 664, 682, 506, 615, 617, 559, 619, 507* | ⊢  |
| | : , : , : , : , : , :  |
| 491 | instantiation | 508, 509 | ⊢  |
| | : , : , :  |
| 492 | theorem | | ⊢  |
| | proveit.logic.equality.equals_reversal |
| 493 | instantiation | 510, 527 | ⊢  |
| | : , :  |
| 494 | axiom | | ⊢  |
| | proveit.physics.quantum.QPE._s_in_nat_pos |
| 495 | instantiation | 511, 512 | ⊢  |
| | : , :  |
| 496 | instantiation | 685, 635, 513 | ⊢  |
| | : , : , :  |
| 497 | instantiation | 514, 533, 515, 516 | , ⊢  |
| | : , : , : , :  |
| 498 | instantiation | 685, 686, 517 | ⊢  |
| | : , : , :  |
| 499 | instantiation | 685, 652, 518 | , ⊢  |
| | : , : , :  |
| 500 | instantiation | 584, 519, 520 | ⊢  |
| | : , : , :  |
| 501 | instantiation | 540, 682, 614, 610, 615, 521, 619, 559, 617, 522* | ⊢  |
| | : , : , : , : , : , :  |
| 502 | conjecture | | ⊢  |
| | proveit.numbers.addition.elim_zero_left |
| 503 | instantiation | 685, 644, 523 | , ⊢  |
| | : , : , :  |
| 504 | instantiation | 609, 610, 664, 557, 612, 617, 559, 619 | ⊢  |
| | : , : , : , : , : , :  |
| 505 | instantiation | 613, 682, 614, 615, 524, 617, 559, 619 | ⊢  |
| | : , : , : , :  |
| 506 | instantiation | 631 | ⊢  |
| | : , :  |
| 507 | instantiation | 578, 577, 525 | ⊢  |
| | : , : , :  |
| 508 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.range_len |
| 509 | instantiation | 526, 527, 528 | ⊢  |
| | : , : , :  |
| 510 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.range_from1_len |
| 511 | conjecture | | ⊢  |
| | proveit.numbers.ordering.relax_less |
| 512 | instantiation | 529, 607, 642, 649, 530, 605* | ⊢  |
| | : , : , :  |
| 513 | instantiation | 685, 638, 531 | ⊢  |
| | : , : , :  |
| 514 | conjecture | | ⊢  |
| | proveit.linear_algebra.addition.binary_closure |
| 515 | conjecture | | ⊢  |
| | proveit.physics.quantum.algebra.ket_zero_in_qubit_space |
| 516 | instantiation | 532, 533, 534, 535 | , ⊢  |
| | : , : , : , :  |
| 517 | instantiation | 663, 664, 536 | ⊢  |
| | : , :  |
| 518 | instantiation | 685, 655, 537 | , ⊢  |
| | : , : , :  |
| 519 | instantiation | 584, 538, 539 | ⊢  |
| | : , : , :  |
| 520 | instantiation | 558, 664, 610, 682, 541, 615, 619, 559, 617 | ⊢  |
| | : , : , : , : , : , : , :  |
| 521 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 522 | instantiation | 540, 682, 664, 610, 615, 541, 619, 559, 542* | ⊢  |
| | : , : , : , : , : , :  |
| 523 | assumption | | ⊢  |
| 524 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 525 | instantiation | 606, 619, 559 | ⊢  |
| | : , :  |
| 526 | theorem | | ⊢  |
| | proveit.logic.equality.sub_left_side_into |
| 527 | instantiation | 685, 543, 689 | ⊢  |
| | : , : , :  |
| 528 | instantiation | 584, 544, 545 | ⊢  |
| | : , : , :  |
| 529 | conjecture | | ⊢  |
| | proveit.numbers.ordering.less_shift_add_right |
| 530 | instantiation | 546, 684 | ⊢  |
| | :  |
| 531 | instantiation | 547, 548, 588, 549 | ⊢  |
| | : , :  |
| 532 | conjecture | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.scalar_mult_closure |
| 533 | instantiation | 550, 666 | ⊢  |
| | :  |
| 534 | instantiation | 685, 551, 552 | , ⊢  |
| | : , : , :  |
| 535 | conjecture | | ⊢  |
| | proveit.physics.quantum.algebra.ket_one_in_qubit_space |
| 536 | instantiation | 553, 554, 555 | ⊢  |
| | :  |
| 537 | instantiation | 685, 686, 556 | , ⊢  |
| | : , : , :  |
| 538 | instantiation | 609, 610, 664, 557, 619, 617, 559 | ⊢  |
| | : , : , : , : , : , :  |
| 539 | instantiation | 558, 610, 619, 617, 559 | ⊢  |
| | : , : , : , : , : , : , :  |
| 540 | conjecture | | ⊢  |
| | proveit.numbers.addition.association |
| 541 | instantiation | 631 | ⊢  |
| | : , :  |
| 542 | instantiation | 584, 560, 561 | ⊢  |
| | : , : , :  |
| 543 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat |
| 544 | instantiation | 576, 562 | ⊢  |
| | : , : , :  |
| 545 | instantiation | 584, 563, 564 | ⊢  |
| | : , : , :  |
| 546 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.negative_if_in_neg_int |
| 547 | conjecture | | ⊢  |
| | proveit.numbers.division.div_real_pos_closure |
| 548 | instantiation | 685, 636, 565 | ⊢  |
| | : , : , :  |
| 549 | instantiation | 566, 567 | ⊢  |
| | :  |
| 550 | conjecture | | ⊢  |
| | proveit.linear_algebra.complex_vec_set_is_vec_space |
| 551 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.complex_nonzero_within_complex |
| 552 | instantiation | 568, 569, 570 | , ⊢  |
| | : , :  |
| 553 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.nonneg_int_is_natural |
| 554 | instantiation | 678, 656, 571 | ⊢  |
| | : , :  |
| 555 | instantiation | 572, 573 | ⊢  |
| | : , :  |
| 556 | instantiation | 663, 664, 574 | , ⊢  |
| | : , :  |
| 557 | instantiation | 631 | ⊢  |
| | : , :  |
| 558 | conjecture | | ⊢  |
| | proveit.numbers.addition.leftward_commutation |
| 559 | instantiation | 685, 635, 575 | ⊢  |
| | : , : , :  |
| 560 | instantiation | 576, 577 | ⊢  |
| | : , : , :  |
| 561 | instantiation | 578, 579, 580 | ⊢  |
| | : , : , :  |
| 562 | instantiation | 581, 582, 619, 583* | ⊢  |
| | : , :  |
| 563 | instantiation | 584, 585, 586 | ⊢  |
| | : , : , :  |
| 564 | instantiation | 587, 619, 617 | ⊢  |
| | : , :  |
| 565 | instantiation | 685, 650, 687 | ⊢  |
| | : , : , :  |
| 566 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero |
| 567 | instantiation | 685, 622, 588 | ⊢  |
| | : , : , :  |
| 568 | conjecture | | ⊢  |
| | proveit.numbers.exponentiation.exp_complex_nonzero_closure |
| 569 | instantiation | 685, 589, 590 | ⊢  |
| | : , : , :  |
| 570 | instantiation | 591, 592, 593, 602, 594, 595, 596, 597 | , ⊢  |
| | : , :  |
| 571 | instantiation | 685, 683, 598 | ⊢  |
| | : , : , :  |
| 572 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.nonneg_difference |
| 573 | instantiation | 599, 689 | ⊢  |
| | :  |
| 574 | instantiation | 667, 600 | , ⊢  |
| | :  |
| 575 | instantiation | 648, 630 | ⊢  |
| | :  |
| 576 | axiom | | ⊢  |
| | proveit.logic.equality.substitution |
| 577 | instantiation | 601, 619, 602, 603 | ⊢  |
| | : , : , :  |
| 578 | theorem | | ⊢  |
| | proveit.logic.equality.sub_right_side_into |
| 579 | instantiation | 604, 612, 619, 605 | ⊢  |
| | : , : , :  |
| 580 | instantiation | 606, 619, 618 | ⊢  |
| | : , :  |
| 581 | conjecture | | ⊢  |
| | proveit.numbers.negation.distribute_neg_through_binary_sum |
| 582 | instantiation | 685, 635, 607 | ⊢  |
| | : , : , :  |
| 583 | instantiation | 608, 617 | ⊢  |
| | :  |
| 584 | axiom | | ⊢  |
| | proveit.logic.equality.equals_transitivity |
| 585 | instantiation | 609, 610, 664, 611, 612, 617, 618, 619 | ⊢  |
| | : , : , : , : , : , :  |
| 586 | instantiation | 613, 682, 614, 615, 616, 617, 618, 619 | ⊢  |
| | : , : , : , :  |
| 587 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_triple_32 |
| 588 | instantiation | 620, 621 | ⊢  |
| | :  |
| 589 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero |
| 590 | instantiation | 685, 622, 623 | ⊢  |
| | : , : , :  |
| 591 | conjecture | | ⊢  |
| | proveit.numbers.multiplication.mult_complex_closure |
| 592 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.nat5 |
| 593 | instantiation | 624 | ⊢  |
| | : , : , : , : , :  |
| 594 | instantiation | 685, 635, 625 | ⊢  |
| | : , : , :  |
| 595 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.i_is_complex |
| 596 | instantiation | 685, 635, 626 | , ⊢  |
| | : , : , :  |
| 597 | instantiation | 685, 635, 627 | ⊢  |
| | : , : , :  |
| 598 | instantiation | 688, 687 | ⊢  |
| | :  |
| 599 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound |
| 600 | instantiation | 669, 628, 629 | , ⊢  |
| | :  |
| 601 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.subtract_from_add_reversed |
| 602 | instantiation | 685, 635, 630 | ⊢  |
| | : , : , :  |
| 603 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.add_1_1 |
| 604 | conjecture | | ⊢  |
| | proveit.numbers.addition.subtraction.subtract_from_add |
| 605 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.add_0_1 |
| 606 | conjecture | | ⊢  |
| | proveit.numbers.addition.commutation |
| 607 | instantiation | 648, 633 | ⊢  |
| | :  |
| 608 | conjecture | | ⊢  |
| | proveit.numbers.negation.double_negation |
| 609 | conjecture | | ⊢  |
| | proveit.numbers.addition.disassociation |
| 610 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat1 |
| 611 | instantiation | 631 | ⊢  |
| | : , :  |
| 612 | instantiation | 685, 635, 642 | ⊢  |
| | : , : , :  |
| 613 | conjecture | | ⊢  |
| | proveit.numbers.addition.elim_zero_any |
| 614 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.nat3 |
| 615 | conjecture | | ⊢  |
| | proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
| 616 | instantiation | 632 | ⊢  |
| | : , : , :  |
| 617 | instantiation | 685, 635, 633 | ⊢  |
| | : , : , :  |
| 618 | instantiation | 685, 635, 634 | ⊢  |
| | : , : , :  |
| 619 | instantiation | 685, 635, 649 | ⊢  |
| | : , : , :  |
| 620 | conjecture | | ⊢  |
| | proveit.numbers.exponentiation.sqrt_real_pos_closure |
| 621 | instantiation | 685, 636, 637 | ⊢  |
| | : , : , :  |
| 622 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero |
| 623 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.e_is_real_pos |
| 624 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_5_typical_eq |
| 625 | instantiation | 685, 638, 639 | ⊢  |
| | : , : , :  |
| 626 | instantiation | 685, 652, 640 | , ⊢  |
| | : , : , :  |
| 627 | instantiation | 641, 642, 649, 643 | ⊢  |
| | : , : , :  |
| 628 | instantiation | 685, 644, 645 | , ⊢  |
| | : , : , :  |
| 629 | instantiation | 673, 654, 677, 645 | , ⊢  |
| | : , : , :  |
| 630 | instantiation | 685, 652, 646 | ⊢  |
| | : , : , :  |
| 631 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
| 632 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_3_typical_eq |
| 633 | instantiation | 685, 652, 647 | ⊢  |
| | : , : , :  |
| 634 | instantiation | 648, 649 | ⊢  |
| | :  |
| 635 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.real_within_complex |
| 636 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos |
| 637 | instantiation | 685, 650, 666 | ⊢  |
| | : , : , :  |
| 638 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.real_pos_within_real |
| 639 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.pi_is_real_pos |
| 640 | instantiation | 685, 655, 651 | , ⊢  |
| | : , : , :  |
| 641 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real |
| 642 | instantiation | 685, 652, 653 | ⊢  |
| | : , : , :  |
| 643 | axiom | | ⊢  |
| | proveit.physics.quantum.QPE._phase_in_interval |
| 644 | instantiation | 675, 654, 677 | ⊢  |
| | : , :  |
| 645 | assumption | | ⊢  |
| 646 | instantiation | 685, 655, 660 | ⊢  |
| | : , : , :  |
| 647 | instantiation | 685, 655, 656 | ⊢  |
| | : , : , :  |
| 648 | conjecture | | ⊢  |
| | proveit.numbers.negation.real_closure |
| 649 | instantiation | 657, 658, 687 | ⊢  |
| | : , : , :  |
| 650 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos |
| 651 | instantiation | 685, 686, 659 | , ⊢  |
| | : , : , :  |
| 652 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.rational_within_real |
| 653 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.rational_numbers.zero_is_rational |
| 654 | instantiation | 678, 679, 660 | ⊢  |
| | : , :  |
| 655 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.rational_numbers.int_within_rational |
| 656 | instantiation | 685, 686, 689 | ⊢  |
| | : , : , :  |
| 657 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.unfold_subset_eq |
| 658 | instantiation | 661, 662 | ⊢  |
| | : , :  |
| 659 | instantiation | 663, 664, 665 | , ⊢  |
| | : , :  |
| 660 | instantiation | 685, 686, 666 | ⊢  |
| | : , : , :  |
| 661 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.relax_proper_subset |
| 662 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.nat_pos_within_real |
| 663 | conjecture | | ⊢  |
| | proveit.numbers.exponentiation.exp_natpos_closure |
| 664 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat2 |
| 665 | instantiation | 667, 668 | , ⊢  |
| | :  |
| 666 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat2 |
| 667 | conjecture | | ⊢  |
| | proveit.numbers.negation.nat_closure |
| 668 | instantiation | 669, 670, 671 | , ⊢  |
| | :  |
| 669 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos |
| 670 | instantiation | 685, 672, 674 | , ⊢  |
| | : , : , :  |
| 671 | instantiation | 673, 676, 677, 674 | , ⊢  |
| | : , : , :  |
| 672 | instantiation | 675, 676, 677 | ⊢  |
| | : , :  |
| 673 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.interval_upper_bound |
| 674 | assumption | | ⊢  |
| 675 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.int_interval_within_int |
| 676 | instantiation | 678, 679, 680 | ⊢  |
| | : , :  |
| 677 | instantiation | 685, 681, 682 | ⊢  |
| | : , : , :  |
| 678 | conjecture | | ⊢  |
| | proveit.numbers.addition.add_int_closure_bin |
| 679 | instantiation | 685, 683, 684 | ⊢  |
| | : , : , :  |
| 680 | instantiation | 685, 686, 687 | ⊢  |
| | : , : , :  |
| 681 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.nat_within_int |
| 682 | axiom | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.zero_in_nats |
| 683 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.neg_int_within_int |
| 684 | instantiation | 688, 689 | ⊢  |
| | :  |
| 685 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
| 686 | conjecture | | ⊢  |
| | proveit.numbers.number_sets.integers.nat_pos_within_int |
| 687 | conjecture | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat1 |
| 688 | conjecture | | ⊢  |
| | proveit.numbers.negation.int_neg_closure |
| 689 | assumption | | ⊢  |
| *equality replacement requirements |